package systemf;

/**
   * Following typechecking as in Types and Programming Languages by Benjamin Pierce, chap 9-10-11-23-24-25
   *
   */



trait SystemFTypeCheck extends TypeChecker {self: TypeChecker with SubstitutionProvider =>


  def typeOf(t:LTerm)  = Typer.fresh.typeOf(t)

  object Typer {
    def fresh() = new SystemFTyperFun { val ctx = new Context(Nil) }
  }

  trait Typer extends Function1[LTerm, LType] {
    val ctx: Context
    def withExtendedScope(str: String, b:VarBinding) = {
          val ctx2 = ctx + (str,b)
          create(ctx2) //writing new Typer{ val ctx = this.ctx }gives recursive value error
    }
    def withExtendedScope(str: String, b:TypeVarBinding) = {
      val ctx2 = ctx + (str,b)
      create(ctx2)//new Typer { val ctx = ctx2 } 
    }
    
    def lookupVar(n: Int) = ctx(n)

    def apply(t:LTerm):LType = { typeOf(t) }

    def typeOf(t: LTerm): LType
    def create(ctx: Context): Typer
  }

  
  
  
  trait SystemFTyperFun extends Typer {
    def create(initctx: Context)= {
      new SystemFTyperFun {val ctx = initctx}
    }
    def typeOf(t: LTerm)= t match {
      
        case base:BaseValue => base.baseType
        
        case If(cond,pos,neg) => {
           if (TyBool != typeOf(cond)) throw new TypeExc("conditional not boolean")
           val typpos = typeOf(pos)
           if ( typpos != typeOf(neg)) throw new TypeExc("branches of if differ in type: "+typeOf(pos)+" vs "+typeOf(neg))
           typpos
        }

        case r@Record(fields)       => { 
           TyRecord(r.map(typeOf))
        }
        case RecProj(t,label) => {
        typeOf(t) match {
          case r@TyRecord(fields) =>
               r.field(label)
          case _         => throw new TypeExc("trying to project a non record")
        }
        
        }
        
        
        case Let(VarName(str),t1,t2) => {
          val typeInsert = typeOf(t1)
          removingBinder(withExtendedScope(str, new VarBinding(typeInsert)).typeOf(t2))
        }
        
        case Var(n)       =>   { //T-Var
          lookupVar(n) match {
          case b:Some[VarBinding] => b.get.ltype
          case _                    => throw new TypeExc("unknown var: "+n)
        }
        }
        
        
        case Lam(x,ty,t) => {  //T-Abs
        //val ctx2  = ctx + (x,new VarBinding(ty))
        TyArr(ty, removingBinder(withExtendedScope(x, new VarBinding(ty)) typeOf(t)  )) //we are leaving the deeper scope so have to shift one
        }
        case App(t1,t2)  => {  //T-App
        val ty1 = typeOf(t1)
        val ty2 = typeOf(t2)
        ty1 match {
          case TyArr(ty1D, ty1G) => {  
            if  (ty2 == ty1D ) ty1G
            else throw new TypeExc("receive "+ (if(ty2==null) "untyped" else ty2) 
                +" but expect "+ (if(ty1D==null)"" else ty1D))
          }
          case _                 => {
            throw new TypeExc("applying to non function type")
          }
        }
        }
        
        
        case TLam(x,t)   => {  //T-TAbs
          TyUniv(x, withExtendedScope(x, new TypeVarBinding(x)) typeOf(t))
        }
        case TApp(t, ty) => {  //T-TApp
          val ttype = typeOf(t)
          ttype match {
            case TyUniv(x, ty12) =>
              val result = substitutetype(ty).asTop.intotype(ty12)
              result
            case _  => throw new TypeExc("applying type to non universal type")
        }
        }
        case Pack(privtype,privimpl,sig) => { //T-Pack
          sig match {
          case TyExist(varname,ty) =>
            val tyconcrete = substitutetype(privtype).asTop.intotype(ty)
            val impltype = typeOf(privimpl)
            if (impltype == tyconcrete) TyExist(varname,ty)
            else throw new TypeExc("type of "+privimpl+"="+impltype+" does not match public type "+ty)
          case _ => throw new TypeExc("cannot pack as non-existential type")
        }
        }
        
      case Unpack(pack,tyX,varx,body) => { //T-Unpack
        val impltype = typeOf(pack) //really look at it to force checks made under case Pack
        impltype match {
          case TyExist(tyX2, tyvarx) =>//if tyX == tyX2 =>
           val tybody = withExtendedScope(tyX, new TypeVarBinding(tyX)).withExtendedScope(varx, new VarBinding(tyvarx))
                            .typeOf(body)
           try {
           val tyextern  = removingBinder(removingBinder(tybody)) //view outside of double binder existential
           // we should not be referencing the newly bound var => only be referencing vars in the context outside of the binders
           //val freeextern = freetypes(tyextern)
           //freeextern.foreach({case TyVar(n) => if (lookupVar(n) isEmpty) throw new TypeExc("leaking type variable out of import in "+t.toString)})
           //catch {case e:IllegalArgumentException => throw new TypeExc("leaking type variable out of import in "+t.toString)}
           
           tyextern
           } catch {case e: IllegalArgumentException =>
             throw new TypeExc("leaking type variable out of import in "+t.toString)
           }
      
           
       // case TyExist(a,b)                         => //not necessary, type variables may differ
       //    throw new TypeExc("cannot unpack existential type with different signature ")
          case _ => throw new TypeExc("cannot unpack non existential type ")
            
      }}
   }
  
  }
    
    
}

